A:Type, n, m:, f:(A(A + Top)), x:A.
(can-apply(f^n+m;x))  ((can-apply(f^m;x)) & (can-apply(f^n;do-apply(f^m;x)))) 

latex

ProofTree

Definitions

s = t, t  T, Type, , left + right, x:AB(x), b, {x:A| B(x)} , case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , Top, f^n, can-apply(f;x), , A c B, P & Q, x:A  B(x), P  Q, P  Q, A  B, False, A, , n+m, a < b, Void, x:A. B(x), S  T, suptype(S; T), P  Q, do-apply(f;x), {T}, f o g  , True, x:A.B(x), T, , ff, b, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, [d], p  q, p  q, p q, tt, Unit

Lemmas

eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, bool wf, squash wf, true wf, p-fun-exp-add, can-apply-fun-exp-add, iff wf, can-apply wf, p-fun-exp wf, top wf, nat wf, member wf, le wf, rev implies wf, assert wf